(set-logic QF_NRA)
(set-info :source |Benchmarks generated from hycomp (https://es-static.fbk.eu/tools/hycomp/). BMC instances of non-linear hybrid automata taken from: Alessandro Cimatti, Sergio Mover, Stefano Tonetta, A quantifier-free SMT encoding of non-linear hybrid automata, FMCAD 2012 and Alessandro Cimatti, Sergio Mover, Stefano Tonetta, Quantier-free encoding of invariants for Hybrid Systems, Formal Methods in System Design. This instance solves a BMC problem of depth 6 and uses the encoding obtained with quantifier elimination using qepcad encoding. Contacts: Sergio Mover (mover@fbk.eu), Stefano Tonetta (tonettas@fbk.eu), Alessandro Cimatti (cimatti@fbk.eu).|)
(set-info :smt-lib-version 2.0)
(set-info :category "industrial")
(set-info :status unknown)
;; MathSAT API call trace
;; generated on Mon Mar 19 10:43:33 2012
(declare-fun b.counter.0__AT0 () Bool)
(declare-fun b.EVENT.0__AT6 () Bool)
(declare-fun b.counter.3__AT6 () Bool)
(declare-fun b.counter.2__AT0 () Bool)
(declare-fun b.counter.1__AT0 () Bool)
(declare-fun b.EVENT.1__AT6 () Bool)
(declare-fun b.counter.1__AT1 () Bool)
(declare-fun b.time__AT2 () Real)
(declare-fun b.counter.2__AT1 () Bool)
(declare-fun b.speed_y__AT6 () Real)
(declare-fun b.delta__AT2 () Real)
(declare-fun b.EVENT.0__AT2 () Bool)
(declare-fun speed_loss__AT0 () Real)
(declare-fun b.y__AT2 () Real)
(declare-fun b.EVENT.1__AT2 () Bool)
(declare-fun b.speed_y__AT0 () Real)
(declare-fun b.event_is_timed__AT1 () Bool)
(declare-fun b.counter.0__AT2 () Bool)
(declare-fun b.event_is_timed__AT5 () Bool)
(declare-fun b.event_is_timed__AT0 () Bool)
(declare-fun b.counter.1__AT2 () Bool)
(declare-fun b.counter.3__AT1 () Bool)
(declare-fun b.y__AT5 () Real)
(declare-fun b.delta__AT0 () Real)
(declare-fun b.counter.0__AT5 () Bool)
(declare-fun b.y__AT1 () Real)
(declare-fun b.event_is_timed__AT4 () Bool)
(declare-fun b.time__AT5 () Real)
(declare-fun b.event_is_timed__AT3 () Bool)
(declare-fun b.counter.1__AT5 () Bool)
(declare-fun b.counter.0__AT1 () Bool)
(declare-fun b.counter.3__AT0 () Bool)
(declare-fun b.delta__AT5 () Real)
(declare-fun b.counter.2__AT5 () Bool)
(declare-fun b.speed_y__AT2 () Real)
(declare-fun b.y__AT4 () Real)
(declare-fun b.EVENT.0__AT5 () Bool)
(declare-fun b.y__AT3 () Real)
(declare-fun b.counter.3__AT5 () Bool)
(declare-fun b.delta__AT1 () Real)
(declare-fun b.counter.2__AT2 () Bool)
(declare-fun b.counter.0__AT4 () Bool)
(declare-fun b.EVENT.1__AT5 () Bool)
(declare-fun b.counter.0__AT3 () Bool)
(declare-fun b.EVENT.0__AT1 () Bool)
(declare-fun b.EVENT.1__AT0 () Bool)
(declare-fun b.counter.3__AT2 () Bool)
(declare-fun b.counter.1__AT4 () Bool)
(declare-fun b.time__AT3 () Real)
(declare-fun b.counter.1__AT3 () Bool)
(declare-fun b.EVENT.1__AT1 () Bool)
(declare-fun b.delta__AT4 () Real)
(declare-fun b.EVENT.0__AT0 () Bool)
(declare-fun b.time__AT6 () Real)
(declare-fun b.counter.2__AT4 () Bool)
(declare-fun b.delta__AT3 () Real)
(declare-fun b.event_is_timed__AT6 () Bool)
(declare-fun b.speed_y__AT5 () Real)
(declare-fun b.counter.2__AT3 () Bool)
(declare-fun b.time__AT1 () Real)
(declare-fun b.EVENT.0__AT4 () Bool)
(declare-fun b.time__AT4 () Real)
(declare-fun b.counter.3__AT4 () Bool)
(declare-fun b.EVENT.0__AT3 () Bool)
(declare-fun b.counter.3__AT3 () Bool)
(declare-fun b.speed_y__AT1 () Real)
(declare-fun b.EVENT.1__AT4 () Bool)
(declare-fun b.EVENT.1__AT3 () Bool)
(declare-fun b.time__AT0 () Real)
(declare-fun b.y__AT6 () Real)
(declare-fun b.counter.0__AT6 () Bool)
(declare-fun b.speed_y__AT4 () Real)
(declare-fun b.speed_y__AT3 () Real)
(declare-fun b.counter.1__AT6 () Bool)
(declare-fun b.event_is_timed__AT2 () Bool)
(declare-fun b.y__AT0 () Real)
(declare-fun b.delta__AT6 () Real)
(declare-fun b.counter.2__AT6 () Bool)
(assert (let ((.def_1074 (* 49.0 b.delta__AT6)))
(let ((.def_1075 (* b.delta__AT6 .def_1074)))
(let ((.def_1076 (* (- 1.0) .def_1075)))
(let ((.def_1072 (* 10.0 b.delta__AT6)))
(let ((.def_1073 (* b.speed_y__AT6 .def_1072)))
(let ((.def_1077 (+ .def_1073 .def_1076)))
(let ((.def_1078 (* 10.0 b.y__AT6)))
(let ((.def_1080 (+ .def_1078 .def_1077)))
(let ((.def_1081 (<= 0.0 .def_1080)))
(let ((.def_1056 (<= 0.0 b.y__AT6)))
(let ((.def_1082 (and .def_1056 .def_1081)))
(let ((.def_1070 (<= 0.0 b.delta__AT6)))
(let ((.def_1071 (not .def_1070)))
(let ((.def_1083 (or .def_1071 .def_1082)))
(let ((.def_1053 (not b.EVENT.0__AT6)))
(let ((.def_1051 (not b.EVENT.1__AT6)))
(let ((.def_1067 (and .def_1051 .def_1053)))
(let ((.def_1068 (not .def_1067)))
(let ((.def_1084 (or .def_1068 .def_1083)))
(let ((.def_782 (not b.counter.0__AT5)))
(let ((.def_770 (not b.counter.1__AT5)))
(let ((.def_1060 (and .def_770 .def_782)))
(let ((.def_1063 (or b.counter.3__AT5 .def_1060)))
(let ((.def_777 (not b.counter.2__AT5)))
(let ((.def_1061 (and .def_777 .def_1060)))
(let ((.def_792 (not b.counter.3__AT5)))
(let ((.def_1062 (or .def_792 .def_1061)))
(let ((.def_1064 (and .def_1062 .def_1063)))
(let ((.def_60 (<= speed_loss__AT0 (/ 1 2))))
(let ((.def_57 (<= (/ 1 10) speed_loss__AT0)))
(let ((.def_61 (and .def_57 .def_60)))
(let ((.def_1057 (and .def_61 .def_1056)))
(let ((.def_1054 (or .def_1051 .def_1053)))
(let ((.def_6 (not b.counter.0__AT6)))
(let ((.def_4 (not b.counter.1__AT6)))
(let ((.def_1044 (or .def_4 .def_6)))
(let ((.def_1048 (or b.counter.3__AT6 .def_1044)))
(let ((.def_1045 (or b.counter.2__AT6 .def_1044)))
(let ((.def_9 (not b.counter.2__AT6)))
(let ((.def_1043 (or .def_6 .def_9)))
(let ((.def_1046 (and .def_1043 .def_1045)))
(let ((.def_12 (not b.counter.3__AT6)))
(let ((.def_1047 (or .def_12 .def_1046)))
(let ((.def_1049 (and .def_1047 .def_1048)))
(let ((.def_1055 (and .def_1049 .def_1054)))
(let ((.def_1058 (and .def_1055 .def_1057)))
(let ((.def_911 (<= 0.0 b.delta__AT5)))
(let ((.def_894 (not b.EVENT.0__AT5)))
(let ((.def_892 (not b.EVENT.1__AT5)))
(let ((.def_908 (and .def_892 .def_894)))
(let ((.def_909 (not .def_908)))
(let ((.def_1039 (or .def_909 .def_911)))
(let ((.def_1040 (or b.EVENT.1__AT5 .def_1039)))
(let ((.def_973 (= b.counter.0__AT6 b.counter.0__AT5)))
(let ((.def_971 (= b.counter.1__AT6 b.counter.1__AT5)))
(let ((.def_969 (= b.counter.2__AT6 b.counter.2__AT5)))
(let ((.def_968 (= b.counter.3__AT6 b.counter.3__AT5)))
(let ((.def_970 (and .def_968 .def_969)))
(let ((.def_972 (and .def_970 .def_971)))
(let ((.def_974 (and .def_972 .def_973)))
(let ((.def_1036 (or .def_909 .def_974)))
(let ((.def_1037 (or b.EVENT.1__AT5 .def_1036)))
(let ((.def_1024 (* (- 5.0) b.speed_y__AT6)))
(let ((.def_1025 (* (- 49.0) b.delta__AT5)))
(let ((.def_1029 (+ .def_1025 .def_1024)))
(let ((.def_1027 (* 5.0 b.speed_y__AT5)))
(let ((.def_1030 (+ .def_1027 .def_1029)))
(let ((.def_1031 (= .def_1030 0.0 )))
(let ((.def_1015 (* b.speed_y__AT5 b.delta__AT5)))
(let ((.def_1016 (* 10.0 .def_1015)))
(let ((.def_1013 (* b.delta__AT5 b.delta__AT5)))
(let ((.def_1014 (* (- 49.0) .def_1013)))
(let ((.def_1017 (+ .def_1014 .def_1016)))
(let ((.def_1018 (* (- 10.0) b.y__AT6)))
(let ((.def_1021 (+ .def_1018 .def_1017)))
(let ((.def_919 (* 10.0 b.y__AT5)))
(let ((.def_1022 (+ .def_919 .def_1021)))
(let ((.def_1023 (= .def_1022 0.0 )))
(let ((.def_1032 (and .def_1023 .def_1031)))
(let ((.def_1033 (or .def_909 .def_1032)))
(let ((.def_979 (= b.y__AT5 b.y__AT6)))
(let ((.def_967 (= b.speed_y__AT5 b.speed_y__AT6)))
(let ((.def_1010 (and .def_967 .def_979)))
(let ((.def_1007 (= b.delta__AT5 0.0 )))
(let ((.def_1008 (and .def_908 .def_1007)))
(let ((.def_1009 (not .def_1008)))
(let ((.def_1011 (or .def_1009 .def_1010)))
(let ((.def_1012 (or b.EVENT.1__AT5 .def_1011)))
(let ((.def_1034 (and .def_1012 .def_1033)))
(let ((.def_989 (= b.time__AT5 b.time__AT6)))
(let ((.def_1001 (and .def_979 .def_989)))
(let ((.def_1002 (and .def_967 .def_1001)))
(let ((.def_1003 (and .def_974 .def_1002)))
(let ((.def_1004 (or .def_892 .def_1003)))
(let ((.def_992 (* (- 1.0) b.time__AT6)))
(let ((.def_995 (+ b.delta__AT5 .def_992)))
(let ((.def_996 (+ b.time__AT5 .def_995)))
(let ((.def_997 (= .def_996 0.0 )))
(let ((.def_998 (or .def_909 .def_997)))
(let ((.def_999 (or b.EVENT.1__AT5 .def_998)))
(let ((.def_990 (or .def_908 .def_989)))
(let ((.def_991 (or b.EVENT.1__AT5 .def_990)))
(let ((.def_1000 (and .def_991 .def_999)))
(let ((.def_1005 (and .def_1000 .def_1004)))
(let ((.def_985 (= .def_909 b.event_is_timed__AT6)))
(let ((.def_983 (= b.event_is_timed__AT5 .def_908)))
(let ((.def_986 (and .def_983 .def_985)))
(let ((.def_975 (and .def_967 .def_974)))
(let ((.def_928 (<= 0.0 b.speed_y__AT5)))
(let ((.def_929 (not .def_928)))
(let ((.def_927 (= b.y__AT5 0.0 )))
(let ((.def_930 (and .def_927 .def_929)))
(let ((.def_976 (or .def_930 .def_975)))
(let ((.def_944 (or .def_6 b.counter.0__AT5)))
(let ((.def_943 (or b.counter.0__AT6 .def_782)))
(let ((.def_945 (and .def_943 .def_944)))
(let ((.def_946 (and .def_4 .def_945)))
(let ((.def_947 (or b.counter.1__AT5 .def_946)))
(let ((.def_942 (or b.counter.1__AT6 .def_770)))
(let ((.def_948 (and .def_942 .def_947)))
(let ((.def_959 (and .def_9 .def_948)))
(let ((.def_960 (or b.counter.2__AT5 .def_959)))
(let ((.def_954 (and .def_4 .def_782)))
(let ((.def_955 (or b.counter.1__AT5 .def_954)))
(let ((.def_956 (and .def_942 .def_955)))
(let ((.def_957 (and b.counter.2__AT6 .def_956)))
(let ((.def_958 (or .def_777 .def_957)))
(let ((.def_961 (and .def_958 .def_960)))
(let ((.def_962 (and b.counter.3__AT6 .def_961)))
(let ((.def_963 (or b.counter.3__AT5 .def_962)))
(let ((.def_949 (and b.counter.2__AT6 .def_948)))
(let ((.def_950 (or b.counter.2__AT5 .def_949)))
(let ((.def_938 (or b.counter.1__AT6 b.counter.1__AT5)))
(let ((.def_936 (and .def_4 b.counter.0__AT6)))
(let ((.def_937 (or .def_770 .def_936)))
(let ((.def_939 (and .def_937 .def_938)))
(let ((.def_940 (and .def_9 .def_939)))
(let ((.def_941 (or .def_777 .def_940)))
(let ((.def_951 (and .def_941 .def_950)))
(let ((.def_952 (and .def_12 .def_951)))
(let ((.def_953 (or .def_792 .def_952)))
(let ((.def_964 (and .def_953 .def_963)))
(let ((.def_932 (* (- 1.0) b.speed_y__AT5)))
(let ((.def_94 (* (- 1.0) speed_loss__AT0)))
(let ((.def_95 (+ 1.0 .def_94)))
(let ((.def_933 (* .def_95 .def_932)))
(let ((.def_935 (= .def_933 b.speed_y__AT6)))
(let ((.def_965 (and .def_935 .def_964)))
(let ((.def_931 (not .def_930)))
(let ((.def_966 (or .def_931 .def_965)))
(let ((.def_977 (and .def_966 .def_976)))
(let ((.def_980 (and .def_977 .def_979)))
(let ((.def_981 (or .def_908 .def_980)))
(let ((.def_982 (or b.EVENT.1__AT5 .def_981)))
(let ((.def_987 (and .def_982 .def_986)))
(let ((.def_1006 (and .def_987 .def_1005)))
(let ((.def_1035 (and .def_1006 .def_1034)))
(let ((.def_1038 (and .def_1035 .def_1037)))
(let ((.def_1041 (and .def_1038 .def_1040)))
(let ((.def_1042 (and .def_892 .def_1041)))
(let ((.def_1059 (and .def_1042 .def_1058)))
(let ((.def_1065 (and .def_1059 .def_1064)))
(let ((.def_915 (* 49.0 b.delta__AT5)))
(let ((.def_916 (* b.delta__AT5 .def_915)))
(let ((.def_917 (* (- 1.0) .def_916)))
(let ((.def_913 (* 10.0 b.delta__AT5)))
(let ((.def_914 (* b.speed_y__AT5 .def_913)))
(let ((.def_918 (+ .def_914 .def_917)))
(let ((.def_921 (+ .def_919 .def_918)))
(let ((.def_922 (<= 0.0 .def_921)))
(let ((.def_897 (<= 0.0 b.y__AT5)))
(let ((.def_923 (and .def_897 .def_922)))
(let ((.def_912 (not .def_911)))
(let ((.def_924 (or .def_912 .def_923)))
(let ((.def_925 (or .def_909 .def_924)))
(let ((.def_615 (not b.counter.0__AT4)))
(let ((.def_603 (not b.counter.1__AT4)))
(let ((.def_901 (and .def_603 .def_615)))
(let ((.def_904 (or b.counter.3__AT4 .def_901)))
(let ((.def_610 (not b.counter.2__AT4)))
(let ((.def_902 (and .def_610 .def_901)))
(let ((.def_625 (not b.counter.3__AT4)))
(let ((.def_903 (or .def_625 .def_902)))
(let ((.def_905 (and .def_903 .def_904)))
(let ((.def_898 (and .def_61 .def_897)))
(let ((.def_895 (or .def_892 .def_894)))
(let ((.def_885 (or .def_770 .def_782)))
(let ((.def_889 (or b.counter.3__AT5 .def_885)))
(let ((.def_886 (or b.counter.2__AT5 .def_885)))
(let ((.def_884 (or .def_777 .def_782)))
(let ((.def_887 (and .def_884 .def_886)))
(let ((.def_888 (or .def_792 .def_887)))
(let ((.def_890 (and .def_888 .def_889)))
(let ((.def_896 (and .def_890 .def_895)))
(let ((.def_899 (and .def_896 .def_898)))
(let ((.def_744 (<= 0.0 b.delta__AT4)))
(let ((.def_727 (not b.EVENT.0__AT4)))
(let ((.def_725 (not b.EVENT.1__AT4)))
(let ((.def_741 (and .def_725 .def_727)))
(let ((.def_742 (not .def_741)))
(let ((.def_880 (or .def_742 .def_744)))
(let ((.def_881 (or b.EVENT.1__AT4 .def_880)))
(let ((.def_814 (= b.counter.0__AT4 b.counter.0__AT5)))
(let ((.def_812 (= b.counter.1__AT4 b.counter.1__AT5)))
(let ((.def_810 (= b.counter.2__AT4 b.counter.2__AT5)))
(let ((.def_809 (= b.counter.3__AT4 b.counter.3__AT5)))
(let ((.def_811 (and .def_809 .def_810)))
(let ((.def_813 (and .def_811 .def_812)))
(let ((.def_815 (and .def_813 .def_814)))
(let ((.def_877 (or .def_742 .def_815)))
(let ((.def_878 (or b.EVENT.1__AT4 .def_877)))
(let ((.def_865 (* (- 5.0) b.speed_y__AT5)))
(let ((.def_866 (* (- 49.0) b.delta__AT4)))
(let ((.def_870 (+ .def_866 .def_865)))
(let ((.def_868 (* 5.0 b.speed_y__AT4)))
(let ((.def_871 (+ .def_868 .def_870)))
(let ((.def_872 (= .def_871 0.0 )))
(let ((.def_856 (* b.speed_y__AT4 b.delta__AT4)))
(let ((.def_857 (* 10.0 .def_856)))
(let ((.def_854 (* b.delta__AT4 b.delta__AT4)))
(let ((.def_855 (* (- 49.0) .def_854)))
(let ((.def_858 (+ .def_855 .def_857)))
(let ((.def_859 (* (- 10.0) b.y__AT5)))
(let ((.def_862 (+ .def_859 .def_858)))
(let ((.def_752 (* 10.0 b.y__AT4)))
(let ((.def_863 (+ .def_752 .def_862)))
(let ((.def_864 (= .def_863 0.0 )))
(let ((.def_873 (and .def_864 .def_872)))
(let ((.def_874 (or .def_742 .def_873)))
(let ((.def_820 (= b.y__AT4 b.y__AT5)))
(let ((.def_808 (= b.speed_y__AT4 b.speed_y__AT5)))
(let ((.def_851 (and .def_808 .def_820)))
(let ((.def_848 (= b.delta__AT4 0.0 )))
(let ((.def_849 (and .def_741 .def_848)))
(let ((.def_850 (not .def_849)))
(let ((.def_852 (or .def_850 .def_851)))
(let ((.def_853 (or b.EVENT.1__AT4 .def_852)))
(let ((.def_875 (and .def_853 .def_874)))
(let ((.def_830 (= b.time__AT4 b.time__AT5)))
(let ((.def_842 (and .def_820 .def_830)))
(let ((.def_843 (and .def_808 .def_842)))
(let ((.def_844 (and .def_815 .def_843)))
(let ((.def_845 (or .def_725 .def_844)))
(let ((.def_833 (* (- 1.0) b.time__AT5)))
(let ((.def_836 (+ b.delta__AT4 .def_833)))
(let ((.def_837 (+ b.time__AT4 .def_836)))
(let ((.def_838 (= .def_837 0.0 )))
(let ((.def_839 (or .def_742 .def_838)))
(let ((.def_840 (or b.EVENT.1__AT4 .def_839)))
(let ((.def_831 (or .def_741 .def_830)))
(let ((.def_832 (or b.EVENT.1__AT4 .def_831)))
(let ((.def_841 (and .def_832 .def_840)))
(let ((.def_846 (and .def_841 .def_845)))
(let ((.def_826 (= .def_742 b.event_is_timed__AT5)))
(let ((.def_824 (= b.event_is_timed__AT4 .def_741)))
(let ((.def_827 (and .def_824 .def_826)))
(let ((.def_816 (and .def_808 .def_815)))
(let ((.def_761 (<= 0.0 b.speed_y__AT4)))
(let ((.def_762 (not .def_761)))
(let ((.def_760 (= b.y__AT4 0.0 )))
(let ((.def_763 (and .def_760 .def_762)))
(let ((.def_817 (or .def_763 .def_816)))
(let ((.def_783 (or b.counter.0__AT4 .def_782)))
(let ((.def_781 (or .def_615 b.counter.0__AT5)))
(let ((.def_784 (and .def_781 .def_783)))
(let ((.def_785 (and .def_770 .def_784)))
(let ((.def_786 (or b.counter.1__AT4 .def_785)))
(let ((.def_780 (or .def_603 b.counter.1__AT5)))
(let ((.def_787 (and .def_780 .def_786)))
(let ((.def_800 (and .def_777 .def_787)))
(let ((.def_801 (or b.counter.2__AT4 .def_800)))
(let ((.def_795 (and .def_615 .def_770)))
(let ((.def_796 (or b.counter.1__AT4 .def_795)))
(let ((.def_797 (and .def_780 .def_796)))
(let ((.def_798 (and b.counter.2__AT5 .def_797)))
(let ((.def_799 (or .def_610 .def_798)))
(let ((.def_802 (and .def_799 .def_801)))
(let ((.def_803 (and b.counter.3__AT5 .def_802)))
(let ((.def_804 (or b.counter.3__AT4 .def_803)))
(let ((.def_788 (and b.counter.2__AT5 .def_787)))
(let ((.def_789 (or b.counter.2__AT4 .def_788)))
(let ((.def_774 (or b.counter.1__AT4 b.counter.1__AT5)))
(let ((.def_772 (and .def_770 b.counter.0__AT5)))
(let ((.def_773 (or .def_603 .def_772)))
(let ((.def_775 (and .def_773 .def_774)))
(let ((.def_778 (and .def_775 .def_777)))
(let ((.def_779 (or .def_610 .def_778)))
(let ((.def_790 (and .def_779 .def_789)))
(let ((.def_793 (and .def_790 .def_792)))
(let ((.def_794 (or .def_625 .def_793)))
(let ((.def_805 (and .def_794 .def_804)))
(let ((.def_765 (* (- 1.0) b.speed_y__AT4)))
(let ((.def_766 (* .def_95 .def_765)))
(let ((.def_768 (= .def_766 b.speed_y__AT5)))
(let ((.def_806 (and .def_768 .def_805)))
(let ((.def_764 (not .def_763)))
(let ((.def_807 (or .def_764 .def_806)))
(let ((.def_818 (and .def_807 .def_817)))
(let ((.def_821 (and .def_818 .def_820)))
(let ((.def_822 (or .def_741 .def_821)))
(let ((.def_823 (or b.EVENT.1__AT4 .def_822)))
(let ((.def_828 (and .def_823 .def_827)))
(let ((.def_847 (and .def_828 .def_846)))
(let ((.def_876 (and .def_847 .def_875)))
(let ((.def_879 (and .def_876 .def_878)))
(let ((.def_882 (and .def_879 .def_881)))
(let ((.def_883 (and .def_725 .def_882)))
(let ((.def_900 (and .def_883 .def_899)))
(let ((.def_906 (and .def_900 .def_905)))
(let ((.def_748 (* 49.0 b.delta__AT4)))
(let ((.def_749 (* b.delta__AT4 .def_748)))
(let ((.def_750 (* (- 1.0) .def_749)))
(let ((.def_746 (* 10.0 b.delta__AT4)))
(let ((.def_747 (* b.speed_y__AT4 .def_746)))
(let ((.def_751 (+ .def_747 .def_750)))
(let ((.def_754 (+ .def_752 .def_751)))
(let ((.def_755 (<= 0.0 .def_754)))
(let ((.def_730 (<= 0.0 b.y__AT4)))
(let ((.def_756 (and .def_730 .def_755)))
(let ((.def_745 (not .def_744)))
(let ((.def_757 (or .def_745 .def_756)))
(let ((.def_758 (or .def_742 .def_757)))
(let ((.def_448 (not b.counter.0__AT3)))
(let ((.def_436 (not b.counter.1__AT3)))
(let ((.def_734 (and .def_436 .def_448)))
(let ((.def_737 (or b.counter.3__AT3 .def_734)))
(let ((.def_443 (not b.counter.2__AT3)))
(let ((.def_735 (and .def_443 .def_734)))
(let ((.def_458 (not b.counter.3__AT3)))
(let ((.def_736 (or .def_458 .def_735)))
(let ((.def_738 (and .def_736 .def_737)))
(let ((.def_731 (and .def_61 .def_730)))
(let ((.def_728 (or .def_725 .def_727)))
(let ((.def_718 (or .def_603 .def_615)))
(let ((.def_722 (or b.counter.3__AT4 .def_718)))
(let ((.def_719 (or b.counter.2__AT4 .def_718)))
(let ((.def_717 (or .def_610 .def_615)))
(let ((.def_720 (and .def_717 .def_719)))
(let ((.def_721 (or .def_625 .def_720)))
(let ((.def_723 (and .def_721 .def_722)))
(let ((.def_729 (and .def_723 .def_728)))
(let ((.def_732 (and .def_729 .def_731)))
(let ((.def_577 (<= 0.0 b.delta__AT3)))
(let ((.def_560 (not b.EVENT.0__AT3)))
(let ((.def_558 (not b.EVENT.1__AT3)))
(let ((.def_574 (and .def_558 .def_560)))
(let ((.def_575 (not .def_574)))
(let ((.def_713 (or .def_575 .def_577)))
(let ((.def_714 (or b.EVENT.1__AT3 .def_713)))
(let ((.def_647 (= b.counter.0__AT3 b.counter.0__AT4)))
(let ((.def_645 (= b.counter.1__AT3 b.counter.1__AT4)))
(let ((.def_643 (= b.counter.2__AT3 b.counter.2__AT4)))
(let ((.def_642 (= b.counter.3__AT3 b.counter.3__AT4)))
(let ((.def_644 (and .def_642 .def_643)))
(let ((.def_646 (and .def_644 .def_645)))
(let ((.def_648 (and .def_646 .def_647)))
(let ((.def_710 (or .def_575 .def_648)))
(let ((.def_711 (or b.EVENT.1__AT3 .def_710)))
(let ((.def_698 (* (- 5.0) b.speed_y__AT4)))
(let ((.def_699 (* (- 49.0) b.delta__AT3)))
(let ((.def_703 (+ .def_699 .def_698)))
(let ((.def_701 (* 5.0 b.speed_y__AT3)))
(let ((.def_704 (+ .def_701 .def_703)))
(let ((.def_705 (= .def_704 0.0 )))
(let ((.def_689 (* b.speed_y__AT3 b.delta__AT3)))
(let ((.def_690 (* 10.0 .def_689)))
(let ((.def_687 (* b.delta__AT3 b.delta__AT3)))
(let ((.def_688 (* (- 49.0) .def_687)))
(let ((.def_691 (+ .def_688 .def_690)))
(let ((.def_692 (* (- 10.0) b.y__AT4)))
(let ((.def_695 (+ .def_692 .def_691)))
(let ((.def_585 (* 10.0 b.y__AT3)))
(let ((.def_696 (+ .def_585 .def_695)))
(let ((.def_697 (= .def_696 0.0 )))
(let ((.def_706 (and .def_697 .def_705)))
(let ((.def_707 (or .def_575 .def_706)))
(let ((.def_653 (= b.y__AT3 b.y__AT4)))
(let ((.def_641 (= b.speed_y__AT3 b.speed_y__AT4)))
(let ((.def_684 (and .def_641 .def_653)))
(let ((.def_681 (= b.delta__AT3 0.0 )))
(let ((.def_682 (and .def_574 .def_681)))
(let ((.def_683 (not .def_682)))
(let ((.def_685 (or .def_683 .def_684)))
(let ((.def_686 (or b.EVENT.1__AT3 .def_685)))
(let ((.def_708 (and .def_686 .def_707)))
(let ((.def_663 (= b.time__AT3 b.time__AT4)))
(let ((.def_675 (and .def_653 .def_663)))
(let ((.def_676 (and .def_641 .def_675)))
(let ((.def_677 (and .def_648 .def_676)))
(let ((.def_678 (or .def_558 .def_677)))
(let ((.def_666 (* (- 1.0) b.time__AT4)))
(let ((.def_669 (+ b.delta__AT3 .def_666)))
(let ((.def_670 (+ b.time__AT3 .def_669)))
(let ((.def_671 (= .def_670 0.0 )))
(let ((.def_672 (or .def_575 .def_671)))
(let ((.def_673 (or b.EVENT.1__AT3 .def_672)))
(let ((.def_664 (or .def_574 .def_663)))
(let ((.def_665 (or b.EVENT.1__AT3 .def_664)))
(let ((.def_674 (and .def_665 .def_673)))
(let ((.def_679 (and .def_674 .def_678)))
(let ((.def_659 (= .def_575 b.event_is_timed__AT4)))
(let ((.def_657 (= b.event_is_timed__AT3 .def_574)))
(let ((.def_660 (and .def_657 .def_659)))
(let ((.def_649 (and .def_641 .def_648)))
(let ((.def_594 (<= 0.0 b.speed_y__AT3)))
(let ((.def_595 (not .def_594)))
(let ((.def_593 (= b.y__AT3 0.0 )))
(let ((.def_596 (and .def_593 .def_595)))
(let ((.def_650 (or .def_596 .def_649)))
(let ((.def_616 (or b.counter.0__AT3 .def_615)))
(let ((.def_614 (or .def_448 b.counter.0__AT4)))
(let ((.def_617 (and .def_614 .def_616)))
(let ((.def_618 (and .def_603 .def_617)))
(let ((.def_619 (or b.counter.1__AT3 .def_618)))
(let ((.def_613 (or .def_436 b.counter.1__AT4)))
(let ((.def_620 (and .def_613 .def_619)))
(let ((.def_633 (and .def_610 .def_620)))
(let ((.def_634 (or b.counter.2__AT3 .def_633)))
(let ((.def_628 (and .def_448 .def_603)))
(let ((.def_629 (or b.counter.1__AT3 .def_628)))
(let ((.def_630 (and .def_613 .def_629)))
(let ((.def_631 (and b.counter.2__AT4 .def_630)))
(let ((.def_632 (or .def_443 .def_631)))
(let ((.def_635 (and .def_632 .def_634)))
(let ((.def_636 (and b.counter.3__AT4 .def_635)))
(let ((.def_637 (or b.counter.3__AT3 .def_636)))
(let ((.def_621 (and b.counter.2__AT4 .def_620)))
(let ((.def_622 (or b.counter.2__AT3 .def_621)))
(let ((.def_607 (or b.counter.1__AT3 b.counter.1__AT4)))
(let ((.def_605 (and .def_603 b.counter.0__AT4)))
(let ((.def_606 (or .def_436 .def_605)))
(let ((.def_608 (and .def_606 .def_607)))
(let ((.def_611 (and .def_608 .def_610)))
(let ((.def_612 (or .def_443 .def_611)))
(let ((.def_623 (and .def_612 .def_622)))
(let ((.def_626 (and .def_623 .def_625)))
(let ((.def_627 (or .def_458 .def_626)))
(let ((.def_638 (and .def_627 .def_637)))
(let ((.def_598 (* (- 1.0) b.speed_y__AT3)))
(let ((.def_599 (* .def_95 .def_598)))
(let ((.def_601 (= .def_599 b.speed_y__AT4)))
(let ((.def_639 (and .def_601 .def_638)))
(let ((.def_597 (not .def_596)))
(let ((.def_640 (or .def_597 .def_639)))
(let ((.def_651 (and .def_640 .def_650)))
(let ((.def_654 (and .def_651 .def_653)))
(let ((.def_655 (or .def_574 .def_654)))
(let ((.def_656 (or b.EVENT.1__AT3 .def_655)))
(let ((.def_661 (and .def_656 .def_660)))
(let ((.def_680 (and .def_661 .def_679)))
(let ((.def_709 (and .def_680 .def_708)))
(let ((.def_712 (and .def_709 .def_711)))
(let ((.def_715 (and .def_712 .def_714)))
(let ((.def_716 (and .def_558 .def_715)))
(let ((.def_733 (and .def_716 .def_732)))
(let ((.def_739 (and .def_733 .def_738)))
(let ((.def_581 (* 49.0 b.delta__AT3)))
(let ((.def_582 (* b.delta__AT3 .def_581)))
(let ((.def_583 (* (- 1.0) .def_582)))
(let ((.def_579 (* 10.0 b.delta__AT3)))
(let ((.def_580 (* b.speed_y__AT3 .def_579)))
(let ((.def_584 (+ .def_580 .def_583)))
(let ((.def_587 (+ .def_585 .def_584)))
(let ((.def_588 (<= 0.0 .def_587)))
(let ((.def_563 (<= 0.0 b.y__AT3)))
(let ((.def_589 (and .def_563 .def_588)))
(let ((.def_578 (not .def_577)))
(let ((.def_590 (or .def_578 .def_589)))
(let ((.def_591 (or .def_575 .def_590)))
(let ((.def_281 (not b.counter.0__AT2)))
(let ((.def_269 (not b.counter.1__AT2)))
(let ((.def_567 (and .def_269 .def_281)))
(let ((.def_570 (or b.counter.3__AT2 .def_567)))
(let ((.def_276 (not b.counter.2__AT2)))
(let ((.def_568 (and .def_276 .def_567)))
(let ((.def_291 (not b.counter.3__AT2)))
(let ((.def_569 (or .def_291 .def_568)))
(let ((.def_571 (and .def_569 .def_570)))
(let ((.def_564 (and .def_61 .def_563)))
(let ((.def_561 (or .def_558 .def_560)))
(let ((.def_551 (or .def_436 .def_448)))
(let ((.def_555 (or b.counter.3__AT3 .def_551)))
(let ((.def_552 (or b.counter.2__AT3 .def_551)))
(let ((.def_550 (or .def_443 .def_448)))
(let ((.def_553 (and .def_550 .def_552)))
(let ((.def_554 (or .def_458 .def_553)))
(let ((.def_556 (and .def_554 .def_555)))
(let ((.def_562 (and .def_556 .def_561)))
(let ((.def_565 (and .def_562 .def_564)))
(let ((.def_410 (<= 0.0 b.delta__AT2)))
(let ((.def_393 (not b.EVENT.0__AT2)))
(let ((.def_391 (not b.EVENT.1__AT2)))
(let ((.def_407 (and .def_391 .def_393)))
(let ((.def_408 (not .def_407)))
(let ((.def_546 (or .def_408 .def_410)))
(let ((.def_547 (or b.EVENT.1__AT2 .def_546)))
(let ((.def_480 (= b.counter.0__AT2 b.counter.0__AT3)))
(let ((.def_478 (= b.counter.1__AT2 b.counter.1__AT3)))
(let ((.def_476 (= b.counter.2__AT2 b.counter.2__AT3)))
(let ((.def_475 (= b.counter.3__AT2 b.counter.3__AT3)))
(let ((.def_477 (and .def_475 .def_476)))
(let ((.def_479 (and .def_477 .def_478)))
(let ((.def_481 (and .def_479 .def_480)))
(let ((.def_543 (or .def_408 .def_481)))
(let ((.def_544 (or b.EVENT.1__AT2 .def_543)))
(let ((.def_531 (* (- 5.0) b.speed_y__AT3)))
(let ((.def_532 (* (- 49.0) b.delta__AT2)))
(let ((.def_536 (+ .def_532 .def_531)))
(let ((.def_534 (* 5.0 b.speed_y__AT2)))
(let ((.def_537 (+ .def_534 .def_536)))
(let ((.def_538 (= .def_537 0.0 )))
(let ((.def_522 (* b.speed_y__AT2 b.delta__AT2)))
(let ((.def_523 (* 10.0 .def_522)))
(let ((.def_520 (* b.delta__AT2 b.delta__AT2)))
(let ((.def_521 (* (- 49.0) .def_520)))
(let ((.def_524 (+ .def_521 .def_523)))
(let ((.def_525 (* (- 10.0) b.y__AT3)))
(let ((.def_528 (+ .def_525 .def_524)))
(let ((.def_418 (* 10.0 b.y__AT2)))
(let ((.def_529 (+ .def_418 .def_528)))
(let ((.def_530 (= .def_529 0.0 )))
(let ((.def_539 (and .def_530 .def_538)))
(let ((.def_540 (or .def_408 .def_539)))
(let ((.def_486 (= b.y__AT2 b.y__AT3)))
(let ((.def_474 (= b.speed_y__AT2 b.speed_y__AT3)))
(let ((.def_517 (and .def_474 .def_486)))
(let ((.def_514 (= b.delta__AT2 0.0 )))
(let ((.def_515 (and .def_407 .def_514)))
(let ((.def_516 (not .def_515)))
(let ((.def_518 (or .def_516 .def_517)))
(let ((.def_519 (or b.EVENT.1__AT2 .def_518)))
(let ((.def_541 (and .def_519 .def_540)))
(let ((.def_496 (= b.time__AT2 b.time__AT3)))
(let ((.def_508 (and .def_486 .def_496)))
(let ((.def_509 (and .def_474 .def_508)))
(let ((.def_510 (and .def_481 .def_509)))
(let ((.def_511 (or .def_391 .def_510)))
(let ((.def_499 (* (- 1.0) b.time__AT3)))
(let ((.def_502 (+ b.delta__AT2 .def_499)))
(let ((.def_503 (+ b.time__AT2 .def_502)))
(let ((.def_504 (= .def_503 0.0 )))
(let ((.def_505 (or .def_408 .def_504)))
(let ((.def_506 (or b.EVENT.1__AT2 .def_505)))
(let ((.def_497 (or .def_407 .def_496)))
(let ((.def_498 (or b.EVENT.1__AT2 .def_497)))
(let ((.def_507 (and .def_498 .def_506)))
(let ((.def_512 (and .def_507 .def_511)))
(let ((.def_492 (= .def_408 b.event_is_timed__AT3)))
(let ((.def_490 (= b.event_is_timed__AT2 .def_407)))
(let ((.def_493 (and .def_490 .def_492)))
(let ((.def_482 (and .def_474 .def_481)))
(let ((.def_427 (<= 0.0 b.speed_y__AT2)))
(let ((.def_428 (not .def_427)))
(let ((.def_426 (= b.y__AT2 0.0 )))
(let ((.def_429 (and .def_426 .def_428)))
(let ((.def_483 (or .def_429 .def_482)))
(let ((.def_449 (or b.counter.0__AT2 .def_448)))
(let ((.def_447 (or .def_281 b.counter.0__AT3)))
(let ((.def_450 (and .def_447 .def_449)))
(let ((.def_451 (and .def_436 .def_450)))
(let ((.def_452 (or b.counter.1__AT2 .def_451)))
(let ((.def_446 (or .def_269 b.counter.1__AT3)))
(let ((.def_453 (and .def_446 .def_452)))
(let ((.def_466 (and .def_443 .def_453)))
(let ((.def_467 (or b.counter.2__AT2 .def_466)))
(let ((.def_461 (and .def_281 .def_436)))
(let ((.def_462 (or b.counter.1__AT2 .def_461)))
(let ((.def_463 (and .def_446 .def_462)))
(let ((.def_464 (and b.counter.2__AT3 .def_463)))
(let ((.def_465 (or .def_276 .def_464)))
(let ((.def_468 (and .def_465 .def_467)))
(let ((.def_469 (and b.counter.3__AT3 .def_468)))
(let ((.def_470 (or b.counter.3__AT2 .def_469)))
(let ((.def_454 (and b.counter.2__AT3 .def_453)))
(let ((.def_455 (or b.counter.2__AT2 .def_454)))
(let ((.def_440 (or b.counter.1__AT2 b.counter.1__AT3)))
(let ((.def_438 (and .def_436 b.counter.0__AT3)))
(let ((.def_439 (or .def_269 .def_438)))
(let ((.def_441 (and .def_439 .def_440)))
(let ((.def_444 (and .def_441 .def_443)))
(let ((.def_445 (or .def_276 .def_444)))
(let ((.def_456 (and .def_445 .def_455)))
(let ((.def_459 (and .def_456 .def_458)))
(let ((.def_460 (or .def_291 .def_459)))
(let ((.def_471 (and .def_460 .def_470)))
(let ((.def_431 (* (- 1.0) b.speed_y__AT2)))
(let ((.def_432 (* .def_95 .def_431)))
(let ((.def_434 (= .def_432 b.speed_y__AT3)))
(let ((.def_472 (and .def_434 .def_471)))
(let ((.def_430 (not .def_429)))
(let ((.def_473 (or .def_430 .def_472)))
(let ((.def_484 (and .def_473 .def_483)))
(let ((.def_487 (and .def_484 .def_486)))
(let ((.def_488 (or .def_407 .def_487)))
(let ((.def_489 (or b.EVENT.1__AT2 .def_488)))
(let ((.def_494 (and .def_489 .def_493)))
(let ((.def_513 (and .def_494 .def_512)))
(let ((.def_542 (and .def_513 .def_541)))
(let ((.def_545 (and .def_542 .def_544)))
(let ((.def_548 (and .def_545 .def_547)))
(let ((.def_549 (and .def_391 .def_548)))
(let ((.def_566 (and .def_549 .def_565)))
(let ((.def_572 (and .def_566 .def_571)))
(let ((.def_414 (* 49.0 b.delta__AT2)))
(let ((.def_415 (* b.delta__AT2 .def_414)))
(let ((.def_416 (* (- 1.0) .def_415)))
(let ((.def_412 (* 10.0 b.delta__AT2)))
(let ((.def_413 (* b.speed_y__AT2 .def_412)))
(let ((.def_417 (+ .def_413 .def_416)))
(let ((.def_420 (+ .def_418 .def_417)))
(let ((.def_421 (<= 0.0 .def_420)))
(let ((.def_396 (<= 0.0 b.y__AT2)))
(let ((.def_422 (and .def_396 .def_421)))
(let ((.def_411 (not .def_410)))
(let ((.def_423 (or .def_411 .def_422)))
(let ((.def_424 (or .def_408 .def_423)))
(let ((.def_112 (not b.counter.0__AT1)))
(let ((.def_100 (not b.counter.1__AT1)))
(let ((.def_400 (and .def_100 .def_112)))
(let ((.def_403 (or b.counter.3__AT1 .def_400)))
(let ((.def_107 (not b.counter.2__AT1)))
(let ((.def_401 (and .def_107 .def_400)))
(let ((.def_122 (not b.counter.3__AT1)))
(let ((.def_402 (or .def_122 .def_401)))
(let ((.def_404 (and .def_402 .def_403)))
(let ((.def_397 (and .def_61 .def_396)))
(let ((.def_394 (or .def_391 .def_393)))
(let ((.def_384 (or .def_269 .def_281)))
(let ((.def_388 (or b.counter.3__AT2 .def_384)))
(let ((.def_385 (or b.counter.2__AT2 .def_384)))
(let ((.def_383 (or .def_276 .def_281)))
(let ((.def_386 (and .def_383 .def_385)))
(let ((.def_387 (or .def_291 .def_386)))
(let ((.def_389 (and .def_387 .def_388)))
(let ((.def_395 (and .def_389 .def_394)))
(let ((.def_398 (and .def_395 .def_397)))
(let ((.def_243 (<= 0.0 b.delta__AT1)))
(let ((.def_228 (not b.EVENT.0__AT1)))
(let ((.def_226 (not b.EVENT.1__AT1)))
(let ((.def_240 (and .def_226 .def_228)))
(let ((.def_241 (not .def_240)))
(let ((.def_379 (or .def_241 .def_243)))
(let ((.def_380 (or b.EVENT.1__AT1 .def_379)))
(let ((.def_313 (= b.counter.0__AT1 b.counter.0__AT2)))
(let ((.def_311 (= b.counter.1__AT1 b.counter.1__AT2)))
(let ((.def_309 (= b.counter.2__AT1 b.counter.2__AT2)))
(let ((.def_308 (= b.counter.3__AT1 b.counter.3__AT2)))
(let ((.def_310 (and .def_308 .def_309)))
(let ((.def_312 (and .def_310 .def_311)))
(let ((.def_314 (and .def_312 .def_313)))
(let ((.def_376 (or .def_241 .def_314)))
(let ((.def_377 (or b.EVENT.1__AT1 .def_376)))
(let ((.def_364 (* (- 5.0) b.speed_y__AT2)))
(let ((.def_365 (* (- 49.0) b.delta__AT1)))
(let ((.def_369 (+ .def_365 .def_364)))
(let ((.def_367 (* 5.0 b.speed_y__AT1)))
(let ((.def_370 (+ .def_367 .def_369)))
(let ((.def_371 (= .def_370 0.0 )))
(let ((.def_355 (* b.speed_y__AT1 b.delta__AT1)))
(let ((.def_356 (* 10.0 .def_355)))
(let ((.def_353 (* b.delta__AT1 b.delta__AT1)))
(let ((.def_354 (* (- 49.0) .def_353)))
(let ((.def_357 (+ .def_354 .def_356)))
(let ((.def_358 (* (- 10.0) b.y__AT2)))
(let ((.def_361 (+ .def_358 .def_357)))
(let ((.def_251 (* 10.0 b.y__AT1)))
(let ((.def_362 (+ .def_251 .def_361)))
(let ((.def_363 (= .def_362 0.0 )))
(let ((.def_372 (and .def_363 .def_371)))
(let ((.def_373 (or .def_241 .def_372)))
(let ((.def_319 (= b.y__AT1 b.y__AT2)))
(let ((.def_307 (= b.speed_y__AT1 b.speed_y__AT2)))
(let ((.def_350 (and .def_307 .def_319)))
(let ((.def_347 (= b.delta__AT1 0.0 )))
(let ((.def_348 (and .def_240 .def_347)))
(let ((.def_349 (not .def_348)))
(let ((.def_351 (or .def_349 .def_350)))
(let ((.def_352 (or b.EVENT.1__AT1 .def_351)))
(let ((.def_374 (and .def_352 .def_373)))
(let ((.def_329 (= b.time__AT1 b.time__AT2)))
(let ((.def_341 (and .def_319 .def_329)))
(let ((.def_342 (and .def_307 .def_341)))
(let ((.def_343 (and .def_314 .def_342)))
(let ((.def_344 (or .def_226 .def_343)))
(let ((.def_332 (* (- 1.0) b.time__AT2)))
(let ((.def_335 (+ b.delta__AT1 .def_332)))
(let ((.def_336 (+ b.time__AT1 .def_335)))
(let ((.def_337 (= .def_336 0.0 )))
(let ((.def_338 (or .def_241 .def_337)))
(let ((.def_339 (or b.EVENT.1__AT1 .def_338)))
(let ((.def_330 (or .def_240 .def_329)))
(let ((.def_331 (or b.EVENT.1__AT1 .def_330)))
(let ((.def_340 (and .def_331 .def_339)))
(let ((.def_345 (and .def_340 .def_344)))
(let ((.def_325 (= .def_241 b.event_is_timed__AT2)))
(let ((.def_323 (= b.event_is_timed__AT1 .def_240)))
(let ((.def_326 (and .def_323 .def_325)))
(let ((.def_315 (and .def_307 .def_314)))
(let ((.def_260 (<= 0.0 b.speed_y__AT1)))
(let ((.def_261 (not .def_260)))
(let ((.def_259 (= b.y__AT1 0.0 )))
(let ((.def_262 (and .def_259 .def_261)))
(let ((.def_316 (or .def_262 .def_315)))
(let ((.def_282 (or b.counter.0__AT1 .def_281)))
(let ((.def_280 (or .def_112 b.counter.0__AT2)))
(let ((.def_283 (and .def_280 .def_282)))
(let ((.def_284 (and .def_269 .def_283)))
(let ((.def_285 (or b.counter.1__AT1 .def_284)))
(let ((.def_279 (or .def_100 b.counter.1__AT2)))
(let ((.def_286 (and .def_279 .def_285)))
(let ((.def_299 (and .def_276 .def_286)))
(let ((.def_300 (or b.counter.2__AT1 .def_299)))
(let ((.def_294 (and .def_112 .def_269)))
(let ((.def_295 (or b.counter.1__AT1 .def_294)))
(let ((.def_296 (and .def_279 .def_295)))
(let ((.def_297 (and b.counter.2__AT2 .def_296)))
(let ((.def_298 (or .def_107 .def_297)))
(let ((.def_301 (and .def_298 .def_300)))
(let ((.def_302 (and b.counter.3__AT2 .def_301)))
(let ((.def_303 (or b.counter.3__AT1 .def_302)))
(let ((.def_287 (and b.counter.2__AT2 .def_286)))
(let ((.def_288 (or b.counter.2__AT1 .def_287)))
(let ((.def_273 (or b.counter.1__AT1 b.counter.1__AT2)))
(let ((.def_271 (and .def_269 b.counter.0__AT2)))
(let ((.def_272 (or .def_100 .def_271)))
(let ((.def_274 (and .def_272 .def_273)))
(let ((.def_277 (and .def_274 .def_276)))
(let ((.def_278 (or .def_107 .def_277)))
(let ((.def_289 (and .def_278 .def_288)))
(let ((.def_292 (and .def_289 .def_291)))
(let ((.def_293 (or .def_122 .def_292)))
(let ((.def_304 (and .def_293 .def_303)))
(let ((.def_264 (* (- 1.0) b.speed_y__AT1)))
(let ((.def_265 (* .def_95 .def_264)))
(let ((.def_267 (= .def_265 b.speed_y__AT2)))
(let ((.def_305 (and .def_267 .def_304)))
(let ((.def_263 (not .def_262)))
(let ((.def_306 (or .def_263 .def_305)))
(let ((.def_317 (and .def_306 .def_316)))
(let ((.def_320 (and .def_317 .def_319)))
(let ((.def_321 (or .def_240 .def_320)))
(let ((.def_322 (or b.EVENT.1__AT1 .def_321)))
(let ((.def_327 (and .def_322 .def_326)))
(let ((.def_346 (and .def_327 .def_345)))
(let ((.def_375 (and .def_346 .def_374)))
(let ((.def_378 (and .def_375 .def_377)))
(let ((.def_381 (and .def_378 .def_380)))
(let ((.def_382 (and .def_226 .def_381)))
(let ((.def_399 (and .def_382 .def_398)))
(let ((.def_405 (and .def_399 .def_404)))
(let ((.def_247 (* 49.0 b.delta__AT1)))
(let ((.def_248 (* b.delta__AT1 .def_247)))
(let ((.def_249 (* (- 1.0) .def_248)))
(let ((.def_245 (* 10.0 b.delta__AT1)))
(let ((.def_246 (* b.speed_y__AT1 .def_245)))
(let ((.def_250 (+ .def_246 .def_249)))
(let ((.def_253 (+ .def_251 .def_250)))
(let ((.def_254 (<= 0.0 .def_253)))
(let ((.def_231 (<= 0.0 b.y__AT1)))
(let ((.def_255 (and .def_231 .def_254)))
(let ((.def_244 (not .def_243)))
(let ((.def_256 (or .def_244 .def_255)))
(let ((.def_257 (or .def_241 .def_256)))
(let ((.def_32 (not b.counter.0__AT0)))
(let ((.def_30 (not b.counter.1__AT0)))
(let ((.def_33 (and .def_30 .def_32)))
(let ((.def_236 (or .def_33 b.counter.3__AT0)))
(let ((.def_38 (not b.counter.3__AT0)))
(let ((.def_35 (not b.counter.2__AT0)))
(let ((.def_36 (and .def_33 .def_35)))
(let ((.def_235 (or .def_36 .def_38)))
(let ((.def_237 (and .def_235 .def_236)))
(let ((.def_232 (and .def_61 .def_231)))
(let ((.def_229 (or .def_226 .def_228)))
(let ((.def_219 (or .def_100 .def_112)))
(let ((.def_223 (or b.counter.3__AT1 .def_219)))
(let ((.def_220 (or b.counter.2__AT1 .def_219)))
(let ((.def_218 (or .def_107 .def_112)))
(let ((.def_221 (and .def_218 .def_220)))
(let ((.def_222 (or .def_122 .def_221)))
(let ((.def_224 (and .def_222 .def_223)))
(let ((.def_230 (and .def_224 .def_229)))
(let ((.def_233 (and .def_230 .def_232)))
(let ((.def_70 (<= 0.0 b.delta__AT0)))
(let ((.def_51 (not b.EVENT.0__AT0)))
(let ((.def_49 (not b.EVENT.1__AT0)))
(let ((.def_67 (and .def_49 .def_51)))
(let ((.def_68 (not .def_67)))
(let ((.def_214 (or .def_68 .def_70)))
(let ((.def_215 (or b.EVENT.1__AT0 .def_214)))
(let ((.def_144 (= b.counter.0__AT0 b.counter.0__AT1)))
(let ((.def_142 (= b.counter.1__AT0 b.counter.1__AT1)))
(let ((.def_140 (= b.counter.2__AT0 b.counter.2__AT1)))
(let ((.def_139 (= b.counter.3__AT0 b.counter.3__AT1)))
(let ((.def_141 (and .def_139 .def_140)))
(let ((.def_143 (and .def_141 .def_142)))
(let ((.def_145 (and .def_143 .def_144)))
(let ((.def_211 (or .def_68 .def_145)))
(let ((.def_212 (or b.EVENT.1__AT0 .def_211)))
(let ((.def_199 (* (- 5.0) b.speed_y__AT1)))
(let ((.def_200 (* (- 49.0) b.delta__AT0)))
(let ((.def_204 (+ .def_200 .def_199)))
(let ((.def_202 (* 5.0 b.speed_y__AT0)))
(let ((.def_205 (+ .def_202 .def_204)))
(let ((.def_206 (= .def_205 0.0 )))
(let ((.def_187 (* b.speed_y__AT0 b.delta__AT0)))
(let ((.def_188 (* 10.0 .def_187)))
(let ((.def_184 (* b.delta__AT0 b.delta__AT0)))
(let ((.def_186 (* (- 49.0) .def_184)))
(let ((.def_189 (+ .def_186 .def_188)))
(let ((.def_191 (* (- 10.0) b.y__AT1)))
(let ((.def_194 (+ .def_191 .def_189)))
(let ((.def_80 (* 10.0 b.y__AT0)))
(let ((.def_195 (+ .def_80 .def_194)))
(let ((.def_196 (= .def_195 0.0 )))
(let ((.def_207 (and .def_196 .def_206)))
(let ((.def_208 (or .def_68 .def_207)))
(let ((.def_150 (= b.y__AT0 b.y__AT1)))
(let ((.def_138 (= b.speed_y__AT0 b.speed_y__AT1)))
(let ((.def_181 (and .def_138 .def_150)))
(let ((.def_178 (= b.delta__AT0 0.0 )))
(let ((.def_179 (and .def_67 .def_178)))
(let ((.def_180 (not .def_179)))
(let ((.def_182 (or .def_180 .def_181)))
(let ((.def_183 (or b.EVENT.1__AT0 .def_182)))
(let ((.def_209 (and .def_183 .def_208)))
(let ((.def_160 (= b.time__AT0 b.time__AT1)))
(let ((.def_172 (and .def_150 .def_160)))
(let ((.def_173 (and .def_138 .def_172)))
(let ((.def_174 (and .def_145 .def_173)))
(let ((.def_175 (or .def_49 .def_174)))
(let ((.def_163 (* (- 1.0) b.time__AT1)))
(let ((.def_166 (+ b.delta__AT0 .def_163)))
(let ((.def_167 (+ b.time__AT0 .def_166)))
(let ((.def_168 (= .def_167 0.0 )))
(let ((.def_169 (or .def_68 .def_168)))
(let ((.def_170 (or b.EVENT.1__AT0 .def_169)))
(let ((.def_161 (or .def_67 .def_160)))
(let ((.def_162 (or b.EVENT.1__AT0 .def_161)))
(let ((.def_171 (and .def_162 .def_170)))
(let ((.def_176 (and .def_171 .def_175)))
(let ((.def_156 (= .def_68 b.event_is_timed__AT1)))
(let ((.def_154 (= b.event_is_timed__AT0 .def_67)))
(let ((.def_157 (and .def_154 .def_156)))
(let ((.def_146 (and .def_138 .def_145)))
(let ((.def_89 (<= 0.0 b.speed_y__AT0)))
(let ((.def_90 (not .def_89)))
(let ((.def_88 (= b.y__AT0 0.0 )))
(let ((.def_91 (and .def_88 .def_90)))
(let ((.def_147 (or .def_91 .def_146)))
(let ((.def_113 (or b.counter.0__AT0 .def_112)))
(let ((.def_111 (or .def_32 b.counter.0__AT1)))
(let ((.def_114 (and .def_111 .def_113)))
(let ((.def_115 (and .def_100 .def_114)))
(let ((.def_116 (or b.counter.1__AT0 .def_115)))
(let ((.def_110 (or .def_30 b.counter.1__AT1)))
(let ((.def_117 (and .def_110 .def_116)))
(let ((.def_130 (and .def_107 .def_117)))
(let ((.def_131 (or b.counter.2__AT0 .def_130)))
(let ((.def_125 (and .def_32 .def_100)))
(let ((.def_126 (or b.counter.1__AT0 .def_125)))
(let ((.def_127 (and .def_110 .def_126)))
(let ((.def_128 (and b.counter.2__AT1 .def_127)))
(let ((.def_129 (or .def_35 .def_128)))
(let ((.def_132 (and .def_129 .def_131)))
(let ((.def_133 (and b.counter.3__AT1 .def_132)))
(let ((.def_134 (or b.counter.3__AT0 .def_133)))
(let ((.def_118 (and b.counter.2__AT1 .def_117)))
(let ((.def_119 (or b.counter.2__AT0 .def_118)))
(let ((.def_104 (or b.counter.1__AT0 b.counter.1__AT1)))
(let ((.def_102 (and .def_100 b.counter.0__AT1)))
(let ((.def_103 (or .def_30 .def_102)))
(let ((.def_105 (and .def_103 .def_104)))
(let ((.def_108 (and .def_105 .def_107)))
(let ((.def_109 (or .def_35 .def_108)))
(let ((.def_120 (and .def_109 .def_119)))
(let ((.def_123 (and .def_120 .def_122)))
(let ((.def_124 (or .def_38 .def_123)))
(let ((.def_135 (and .def_124 .def_134)))
(let ((.def_93 (* (- 1.0) b.speed_y__AT0)))
(let ((.def_96 (* .def_93 .def_95)))
(let ((.def_98 (= .def_96 b.speed_y__AT1)))
(let ((.def_136 (and .def_98 .def_135)))
(let ((.def_92 (not .def_91)))
(let ((.def_137 (or .def_92 .def_136)))
(let ((.def_148 (and .def_137 .def_147)))
(let ((.def_151 (and .def_148 .def_150)))
(let ((.def_152 (or .def_67 .def_151)))
(let ((.def_153 (or b.EVENT.1__AT0 .def_152)))
(let ((.def_158 (and .def_153 .def_157)))
(let ((.def_177 (and .def_158 .def_176)))
(let ((.def_210 (and .def_177 .def_209)))
(let ((.def_213 (and .def_210 .def_212)))
(let ((.def_216 (and .def_213 .def_215)))
(let ((.def_217 (and .def_49 .def_216)))
(let ((.def_234 (and .def_217 .def_233)))
(let ((.def_238 (and .def_234 .def_237)))
(let ((.def_75 (* 49.0 b.delta__AT0)))
(let ((.def_76 (* b.delta__AT0 .def_75)))
(let ((.def_78 (* (- 1.0) .def_76)))
(let ((.def_72 (* 10.0 b.delta__AT0)))
(let ((.def_73 (* b.speed_y__AT0 .def_72)))
(let ((.def_79 (+ .def_73 .def_78)))
(let ((.def_82 (+ .def_80 .def_79)))
(let ((.def_83 (<= 0.0 .def_82)))
(let ((.def_62 (<= 0.0 b.y__AT0)))
(let ((.def_84 (and .def_62 .def_83)))
(let ((.def_71 (not .def_70)))
(let ((.def_85 (or .def_71 .def_84)))
(let ((.def_86 (or .def_68 .def_85)))
(let ((.def_63 (and .def_61 .def_62)))
(let ((.def_52 (or .def_49 .def_51)))
(let ((.def_42 (or .def_30 .def_32)))
(let ((.def_46 (or b.counter.3__AT0 .def_42)))
(let ((.def_43 (or b.counter.2__AT0 .def_42)))
(let ((.def_41 (or .def_32 .def_35)))
(let ((.def_44 (and .def_41 .def_43)))
(let ((.def_45 (or .def_38 .def_44)))
(let ((.def_47 (and .def_45 .def_46)))
(let ((.def_53 (and .def_47 .def_52)))
(let ((.def_64 (and .def_53 .def_63)))
(let ((.def_39 (and .def_36 .def_38)))
(let ((.def_27 (= b.speed_y__AT0 0.0 )))
(let ((.def_24 (= b.y__AT0 10.0 )))
(let ((.def_19 (= b.time__AT0 0.0 )))
(let ((.def_21 (and .def_19 b.event_is_timed__AT0)))
(let ((.def_25 (and .def_21 .def_24)))
(let ((.def_28 (and .def_25 .def_27)))
(let ((.def_40 (and .def_28 .def_39)))
(let ((.def_65 (and .def_40 .def_64)))
(let ((.def_7 (and .def_4 .def_6)))
(let ((.def_14 (or .def_7 b.counter.3__AT6)))
(let ((.def_10 (and .def_7 .def_9)))
(let ((.def_13 (or .def_10 .def_12)))
(let ((.def_15 (and .def_13 .def_14)))
(let ((.def_16 (not .def_15)))
(let ((.def_66 (and .def_16 .def_65)))
(let ((.def_87 (and .def_66 .def_86)))
(let ((.def_239 (and .def_87 .def_238)))
(let ((.def_258 (and .def_239 .def_257)))
(let ((.def_406 (and .def_258 .def_405)))
(let ((.def_425 (and .def_406 .def_424)))
(let ((.def_573 (and .def_425 .def_572)))
(let ((.def_592 (and .def_573 .def_591)))
(let ((.def_740 (and .def_592 .def_739)))
(let ((.def_759 (and .def_740 .def_758)))
(let ((.def_907 (and .def_759 .def_906)))
(let ((.def_926 (and .def_907 .def_925)))
(let ((.def_1066 (and .def_926 .def_1065)))
(let ((.def_1085 (and .def_1066 .def_1084)))
.def_1085)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
(check-sat)
(exit)
